\begin{tabbing}
valid{-}sys(${\it es}$;${\it Config}$;${\it Sys}$;$e$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=chain\_sys\_ind(${\it Sys}$($e$);$x$.existse{-}before(${\it es}$;$e$;$c$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$))\+
\\[0ex]\& ($\uparrow$cchead?(${\it Config}$($c$))))
\\[0ex]\& \=existse{-}before(${\it es}$;$e$;$c$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$))\+
\\[0ex]\& (\=($\uparrow$cctail?(${\it Config}$($c$)))\+
\\[0ex]$\vee$ ($\uparrow$ccsucc?(${\it Config}$($c$)))));$i$,${\it xs}$.existse{-}before(${\it es}$;$e$;$c$.($\uparrow$($c$ $\in_{b}$ ${\it Config}$))
\-\-\\[0ex]\& ($\uparrow$ccpred?(${\it Config}$($c$)))
\\[0ex]\& ccpred{-}id(${\it Config}$($c$)) = $i$ $\in$ Id
\\[0ex]\& \=alle{-}lt(${\it es}$;$e$;${\it e'}$.es{-}locl(${\it es}$; $c$; ${\it e'}$)\+
\\[0ex]$\Rightarrow$ ($\neg$(($\uparrow$(${\it e'}$ $\in_{b}$ ${\it Config}$)) \& ($\uparrow$ccpred?(${\it Config}$(${\it e'}$))))))))
\-\-
\end{tabbing}